In this paper, we examine the logics of essence and accident and attempt to ascertain the extent to which those logics are genuinely formalizing the concepts in which we are interested. We suggest that they are not completely successful as they stand. We diagnose some of the problems and make a suggestion for improvement. We also discuss some issues concerning definability in the formal language.

This paper develops sequent calculi for several classical modal logics. Utilizing a polymodal translation of the standard modal language, we are able to establish a base system for the minimal classical modal logic E from which we generate extensions in a modular manner. Our systems admit contraction and cut admissibility, and allow a systematic proof-search procedure of formal derivations.

We provide a Hilbert-style axiomatization of the logic of , as well as a two-dimensional semantics with respect to which our logics are sound and complete. Our completeness results are quite general, pertaining to all such actuality logics that extend a normal and canonical modal basis. We also show that our logics have the strong finite model property and permit straightforward first-order extensions.